-
Notifications
You must be signed in to change notification settings - Fork 631
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
CoqIDE: Improve find/replace UI (margins, icons) #18523
Conversation
e38accd
to
0ca5639
Compare
dc85911
to
2808666
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The changes here are minor. I think they won't make any significant difference in usability for users. Given that we have limited resources to make and review changes and the many things that deserve to be improved, I hope you'll focus on more impactful changes in the future.
@@ -137,13 +139,16 @@ class finder name (view : GText.view) = | |||
end | |||
|
|||
method private set_not_found () = | |||
find_entry#misc#modify_bg [`NORMAL, `NAME "#F7E6E6"]; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Adding the icon and the tooltip are fine, but I would keep the reddish/pink background after an unsuccessful find because some users may prefer the current behavior. GUI detail preferences are subjective.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The part of it which is not subjective is bug #11024 which was caused by the background color. This is the reason to use icons instead.
|
||
method private set_found () = | ||
find_entry#misc#modify_bg [`NORMAL, `NAME "#BAF9CE"] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same thing, I would keep the green.
let _ = GMisc.label ~text:"Find:" ~xalign:1.0 | ||
~packing:(replace_box#attach | ||
(*~xpadding:3 ~ypadding:3*) ~left:0 ~top:1 (*~fill:`X*)) () in | ||
let _ = GMisc.label ~text:"Replace:" ~xalign:1.0 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The xaligns are not needed?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, because I’m using set_halign
below, which looks more relevant. If using ~xalign:1.0
instead, labels are aligned to the right. If using none of them, labels are centered. According to https://docs.gtk.org/gtk3/property.Label.xalign.html xalign
should correspond to a “labels size allocation,” but well, how it works is less clear to me than halign
.
2808666
to
014fd11
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM.
If there is no objection, I will merge soon.
@coqbot: run full ci |
@coqbot: merge now |
@jfehrle: You cannot merge this PR because:
|
@coqbot: merge now |
By the way, would it be easy to add a way to remove the search/replace window? Currently, the way I use is to detach and delete the detached window, but a one-click way would be convenient. |
Just press Escape. |
Wonderful, I learn new things every day! |
Fixes #11024